\begin{tabbing}
abs{-}fifo\{i:l\}($C$;$T$)(${\it es}$,${\it In}$,${\it Out}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:$C$.\+
\\[0ex]$\exists$\=$f$:\{$e$:E$\mid$ abs{-}R ($i$,$e$)\} $\rightarrow$\{$e$:E$\mid$ $\exists$$j$:$C$. (abs{-}S ($j$,$i$,$e$))\} \+
\\[0ex]($\lambda$$e$.$\exists$$j$:$C$. (abs{-}S ($j$,$i$,$e$)) $\leftarrow\leftarrow$ $f$$--$ $\lambda$$e$.abs{-}R ($i$,$e$)
\\[0ex]\& ($\forall$$e$:\{$e$:E$\mid$ abs{-}R ($i$,$e$)\} , $j$:\{$j$:$C$$\mid$ abs{-}S ($j$,$i$,$f$($e$))\} . (${\it Out}$($e$).2) = (${\it In}$($f$($e$)).2))
\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:\{$e$:E$\mid$ abs{-}R ($i$,$e$)\} , $j$:$C$.\+
\\[0ex](abs{-}S ($j$,$i$,$f$($e$))) $\Rightarrow$ (abs{-}S ($j$,$i$,$f$(${\it e'}$))) $\Rightarrow$ $f$($e$) c$\leq$ $f$(${\it e'}$) $\Rightarrow$ $e$ c$\leq$ ${\it e'}$))
\-\-\-
\end{tabbing}